Section: New Results

Languages and Foundations: Process algebra

Participants : Damien Pous, Alan Schmitt, Jean-Bernard Stefani, Claudio Mezzina, Cinzia di Giusto.

The goal of this work is to study process algebraic foundations for component-based distributed programming. Most of this work takes place in the context of the ANR PiCoq project.

To develop composable abstractions for programming dependable systems, we investigate concurrent reversible models of computation, where arbitrary executions can be reversed, step by step, in a causally consistent way. This year we have continued the study of the reversible higher-order pi-calculus and obtained a new encoding of it in the higher-order pi-calculus which improves on the result we published in Concur 2010 by proving the faithfulness of the encoding with a much finer equivalence relation. We also developed a reversible variant of the higher-order pi-calculus where reversibility can be controlled by means of an explicit rollback primitive [37] . We have proved that this rollback primitive is sound and complete in that it provides a causally consistent and complete reversal of concurrent computations, and we have developed a low-level semantics for this primitive, closer to an actual distributed implementation, which we have proved equivalent to the high-level one. All these results are presented in detail in Claudio Mezzina's forthcoming PhD thesis, and have been developed in cooperation with the INRIA Focus team at the University of Bologna.

An interesting and expressive component model for embedded systems is the BIP component model [58] , developed by J. Sifakis' team at the Verimag Laboratory, which features hierarchical software architectures, explicit constructs for specifying component compositions (glues), and multipoint synchronization under priority constraints. We have begun a process calculus analysis of BIP, with a view to combine the reactive features of BIP with the dynamic reconfiguration features of Fractal. Our first result takes the form of new process calculus, called CAB, which we have proved to be a conservative extension of BIP. CAB also enabled us to study the intrinsic expressivity of the BIP model and to prove that priority constraints are essential to BIP expressivity [34] .

We have made significant progress on the formalization in the Coq proof assistant of a core higher-order $\pi$-calculus, called HOcore [20] . We have in particular adapted a canonical locally nameless representation of binding to handle alpha-conversion in our formalization. Several major theorems of HOcore, in particular the fact that IO-bisimulation is correct in relation to barbed congruence and is decidable. This work has been submitted for publication.

A longer version of our work on untyping theorems and cyclic linear logic has been accepted for publication in LMCS [24] , and a book chapter on up-to techniques for bisimulations, written with Davide Sangiorgi from the INRIA Focus team in Bologna, has been published by Cambdridge University Press [46] .

Together with Filippo Bonchi (LIP, ENS Lyon), we have worked on a new algorithm for checking the language equivalence of non-deterministic finite automata (NFA). This algorithm improves on the standard Hopcroft and Karp' algorithm, by using up-to techniques. The first empirical tests look really promising [47]

Together with Tom Hirschowitz (LAMA, U. de Chambéry), we have worked on a categorical model of CCS, where innocent strategies are pre-sheaves. This work has been presented at the ICE workshop [36] , and a long version has been submitted to SACS.